-
Notifications
You must be signed in to change notification settings - Fork 69
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Dcpos, Free DCPOs #249
Dcpos, Free DCPOs #249
Conversation
If $(P, \le)$ is a DCPO, then any function $f : P \to Q$ which preserves | ||
directed lubs is automatically a monotone map, and, consequently, | ||
Scott-continuous. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
"consequently, Scott-continuous"? Didn't we just assume
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah I see, you're defining Scott-continuous as monotone + preserves directed lubs.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, it's a bit odd, but it makes sense if you view the category of DCPOs as a subcategory of the category of posets.
Description
This PR defines DCPOs and pointed DCPOs, constructs the free DCPO and the free pointed DPCO, and proves some various properties about them.